($\lambda$$b$,$A$,$p$,$q$,$z$. if $b$$\rightarrow$ $p$ else $q$ fi) $\in$ $\mathbb{B}\rightarrow$($A$:Type$\rightarrow$$A$$\rightarrow$$A$$\rightarrow\downarrow$True$\rightarrow$$A$)